Definitions | P ![](../FONT/eq.png) Q, x:A. B(x), pred(e), t T, first(e), b, A, A & B, ![](../FONT/lam.png) x,y. t(x;y), Unit, IdLnk, Id, SWellFounded(R(x;y)), eventlist(pred?;e), x before y l, e < e', Prop, {T}, ![](../FONT/lam.png) x. t(x), WellFnd{i}(A;x,y.R(x;y)), ![](../FONT/not.png) b, , P & Q, P ![](../FONT/if_big.png) Q, SQType(T), P Q, False, R1 => R2, x f y, pred!(e;e'), x.A(x), s = t, sender(e), rcv?(e), R^+ |